|
In foundations of mathematics, univalent foundations is an approach to the foundations of constructive mathematics〔See the discussion of the relationship between classical and constructive mathematics in the univalent foundations in this article.〕 based on the idea that mathematics studies structures on "univalent types" that correspond, under the projection to set-theoretic mathematics, to homotopy types. Univalent foundations are inspired both by the old Platonic ideas of Hermann Grassmann and Georg Cantor and by the "categorical" mathematics in the style of Alexander Grothendieck. It departs from the use of predicate logic as the underlying formal deduction system, replacing it, at the moment, by a version of the Martin-Löf type theory. The development of the univalent foundations is closely related with the development of homotopy type theory. Univalent foundations are compatible with structuralism, if an appropriate (i.e. categorical) notion of mathematical structure is adopted. ==History== The main ideas of the univalent foundations were formulated by Vladimir Voevodsky in 2006/2009. The sole reference for the philosophical connections between the univalent foundations and the earlier ideas are Voevodsky's 2014 Bernays lectures.〔Voevodsky (2014)〕 A more detailed discussion of the history of some of the ideas that contribute to the current state of the univalent foundations can be found at the page on homotopy type theory. A fundamental characteristic of the univalent foundations is that they, when combined with the Martin-Löf type theory, provide a practical system for formalization of modern mathematics. A considerable amount of mathematics has been formalized using this system and modern proof assistants such as Coq and Agda. The first such library called "Foundations" was created by Vladimir Voevodsky in 2010.〔Foundations library, see https://github.com/vladimirias/Foundations〕 Now Foundations is a part of a larger development with several authors called UniMath.〔UniMath library, see https://github.com/UniMath/UniMath〕 Foundations also inspired other libraries of formalized mathematics, such as the HoTT Coq library〔HoTT Coq library, see https://github.com/HoTT/HoTT〕 and HoTT Agda library,〔HoTT Agda library, see https://github.com/HoTT/HoTT-Agda〕 that developed the univalent ideas in new directions. An important milestone for the univalent foundations was the Bourbaki Seminar talk by Thierry Coquand〔Coquand's Bourbaki Lecture (Paper ) and (Video )〕 in June, 2014. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「univalent foundations」の詳細全文を読む スポンサード リンク
|